Nuprl Definition : poset_sig
13,42
postcript
pdf
PosetSig ==
car
:Type
(
eq
:(
car
car
)
(
car
car
))
latex
clarification:
PosetSig{i} ==
car
:Type{i}
(
eq
:(
car
car
)
(
car
car
))
latex
Up
poset
sig
object
directory
Wellformedness Lemmas
poset
sig
wf
Definitions
origin
(eq:(car
car
) (carcar))
(eq:(carcar) (carcar)) (eq:(carcar) (carcar))
(eq:(carcar) (carcar))